\documentstyle[portrait,%
              fancybox,%
              notes,%
              epsfig,%
              alltt,%
              semcolor,
              alltt]{seminar}

\input amssym.def
\input amssym

\newcommand{\nat}{\mbox{$\protect\Bbb N$}}
\newcommand{\num}{\mbox{$\protect\Bbb Z$}}
\newcommand{\rat}{\mbox{$\protect\Bbb Q$}}
\newcommand{\real}{\mbox{$\protect\Bbb R$}}
\newcommand{\complex}{\mbox{$\protect\Bbb C$}}
\newcommand{\xxx}{\mbox{$\protect\Bbb X$}}

\newcommand{\lamb}[1]{\lambda #1.\:}
\newcommand{\eps}[1]{\varepsilon #1.\:}
\newcommand{\all}[1]{\forall #1.\:}
\newcommand{\ex}[1]{\exists #1.\:}
\newcommand{\exu}[1]{\exists! #1.\:}

\newcommand{\True}{\top}
\newcommand{\False}{\bot}
\newcommand{\Not}{\neg}
\newcommand{\And}{\wedge}
\newcommand{\Or}{\vee}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}

\newcommand{\entails}{\vdash}
\newcommand{\proves}{\vdash}

\newcommand{\Ands}{\bigwedge}
\newcommand{\Ors}{\bigvee}

\newcommand{\BQ}{\mbox{$\ulcorner$}}
\newcommand{\BEQ}{\mbox{\raise4pt\hbox{$\ulcorner$}}}
\newcommand{\EQ}{\mbox{$\urcorner$}}
\newcommand{\EEQ}{\mbox{\raise4pt\hbox{$\urcorner$}}}

\newcommand{\QUOTE}[1]{\mbox{$\BQ #1 \EQ$}}
\let\psubset=\subset                    % Pure TeX: thanks to MAJ %
\let\subset=\subseteq

\newcommand{\powerset}{\wp}             % This is pretty dire...  %

\newcommand{\Union}{\cup}
\newcommand{\Inter}{\cap}
\newcommand{\Unions}{\bigcup}
\newcommand{\Inters}{\bigcap}

\newcommand{\proof}{{\bf \noindent Proof:\ }}
\newcommand{\qed}{Q.E.D.}

\newcommand{\Rule}{\infer}

\newcommand{\restrict}{\upharpoonright} % This is lousy and must be fixed! %

\newcommand{\bigsqcap}{\mbox{\Large{$\sqcap$}}}

\newcommand\leb{\lbrack\!\lbrack}
\newcommand\reb{\rbrack\!\rbrack}
\newcommand{\sem}[1]{\leb #1 \reb}

\newcommand{\BA}{\begin{array}[t]{l}}
\newcommand{\EA}{\end{array}}
\newcommand{\sqle}{\sqsubseteq}
\newcommand{\sqlt}{\sqsubset}

\newcommand{\too}{\twoheadrightarrow}

\newcommand{\Los}{{\L}o{\'s}}

% These are from Mike's notes

\def\alphas{\mathrel{\mathop{\longrightarrow}\limits_{\alpha}}}
\def\betas{\mathrel{\mathop{\longrightarrow}\limits_{\beta}}}
\def\etas{\mathrel{\mathop{\longrightarrow}\limits_{\eta}}}

\def\goesto{\longrightarrow}

\newcommand{\defeq}{\stackrel{\bigtriangleup}{=}}

% Sizes

\renewcommand{\slidetopmargin}{0.8in}
\renewcommand{\slidebottommargin}{0.8in}

% Various combinations of one colour on another

\newcommand{\greenonred}[1]%
{\psset{fillcolor=red}\psframebox*[framearc=.3]{\green #1}}

\newcommand{\whiteonred}[1]%
{\psset{fillcolor=red}\psframebox*[framearc=.3]{\white #1}}

\newcommand{\yellowonmagenta}[1]%
{\psset{fillcolor=magenta}\psframebox*[framearc=.3]{\yellow #1}}

\newcommand{\whiteonblack}[1]%
{\psset{fillcolor=black}\psframebox*[framearc=.3]{\white #1}}

\newcommand{\blackonlightgray}[1]%
{\psset{fillcolor=lightgray}\psframebox*[framearc=.3]{\black #1}}

\newcommand{\blueonlightgray}[1]%
{\psset{fillcolor=lightgray}\psframebox*[framearc=.3]{\blue #1}}

\newcommand{\cyanonblack}[1]%
{\psset{fillcolor=black}\psframebox*[framearc=.3]{\cyan #1}}

\newcommand{\blueonyellow}[1]%
{\psset{fillcolor=yellow}\psframebox*[framearc=.3]{\blue #1}}

\newcommand{\redonyellow}[1]%
{\psset{fillcolor=yellow}\psframebox*[framearc=.3]{\red #1}}

\newcommand{\heading}[1]%
{\begin{center}\whiteonblack{\large\bf\blueonlightgray{#1}}\end{center}}

\newcommand{\emphatic}[1]{\blueonyellow{#1}}

\newcommand{\veryemphatic}[1]%
{\begin{center}{\emphatic{#1}}\end{center}}

% Head and foot of slides

\newpagestyle{ColourDemo}%
  {\cyanonblack{Introduction to Functional Programming:
                Lecture 6}\hfil\cyanonblack{\thepage}}
  {\cyanonblack{John Harrison}\hfil
   \cyanonblack{University of Cambridge, 28 January 1997}}

\pagestyle{ColourDemo}

\centerslidesfalse

% Colour bullets

\def\labelitemi{{\black$\bullet$}}
\def\labelitemii{{\black--}}
\def\labelitemiii{{\black$\ast$}}
\def\labelitemiv{{\black$\cdot$}}

% Start of document (default text colour is blue)

\begin{document}\blue


\begin{slide*}

\heading{%
\begin{tabular}{c}
{\LARGE\red Introduction to}\\
{\LARGE\red Functional Programming}\\
{\cyan John Harrison}\\
{\cyan University of Cambridge}\\
{\green Lecture 6}\\
{\green Details of ML}
\end{tabular}}

\vspace*{0.5cm}

Topics covered:

\begin{itemize}

\item Interaction with ML; loading files

\item Basic datatypes and operators

\item Infixes and concrete syntax

\item Further examples

\item Defining new types

\end{itemize}

\end{slide*}




\begin{slide*}

\heading{Interaction with ML}

\vspace*{0.5cm}

We have just been typing things into ML and thinking about the results. However
one doesn't write real programs in this way.

Typically, one writes the expressions and declarations in a file. To try them
out as you go, these can be inserted in the ML window using cut and paste.

You can cut and paste using X-windows and similar systems, or an editor like
Emacs with multiple buffers.

For larger programs, it's convenient simply to load them from file into the ML
session. This can be done using the {\black \tt include} command in ML.

\end{slide*}

\begin{slide*}

\heading{Loading from files (1)}

\vspace*{0.5cm}

Suppose that the file {\black \tt myprog.ml} contains the following lines:

\begin{black}\begin{verbatim}
  let pythag x y z =
    x * x + y * y = z * z;;

  pythag 3 4 5;;

  pythag 5 12 13;;

  pythag 1 2 3;;
\end{verbatim}\end{black}

\end{slide*}



\begin{slide*}

\heading{Loading from files (2)}

\vspace*{0.5cm}

Using {\black \tt include} on this file results in the following:

\begin{black}\begin{verbatim}
  #include "myprog.ml";;
  pythag : int -> int -> int -> bool = <fun>
  - : bool = true
  - : bool = true
  - : bool = false
  - : unit = ()
\end{verbatim}\end{black}

ML responds just as if the file had been typed in at the top level.

Normally, the inclusion process terminates as soon as an error is encountered.
The error message is accompanied by a line number.

The final line is the return from the {\black \tt include} command itself. It
has type {\black \tt string -> unit}.

It is permissible to nest inclusions.

\end{slide*}



\begin{slide*}

\heading{Comments}

\vspace*{0.5cm}

Comments are written between {\black \tt (*} and {\black \tt *)}, e.g.

\begin{black}\begin{verbatim}
  (* ----------------------------------- *)
  (* Is (x,y,z) is a Pythagorean triple? *)
  (* ----------------------------------- *)

  let pythag x y z =
      x * x + y * y = z * z;;

  (*comments*) pythag (*can*) 3 (*go*) 4
  (*almost*) 5 (*anywhere*)
  (* and (* can (* be (* nested *)
  quite *) arbitrarily *) *);;
\end{verbatim}\end{black}

The comments are ignored by ML, but are useful for people reading the code.

\end{slide*}




\begin{slide*}

\heading{Basic datatypes}

\vspace*{0.5cm}

The main primitive types are:

\begin{itemize}

\item Type {\black \tt unit}, a 1-element type, whose only element is written
{\black \tt ()}.

\item Type {\black \tt bool}, a 2-element type whose elements are written
{\black \tt true} and {\black \tt false}.

\item Type {\black \tt int}, a subset of the positive and negative integers,
written for example {\black \tt 6} and {\black \tt -11}.

\item Type {\black \tt string}, which corresponds to sequences of characters,
written {\black \tt "like this"}.

\end{itemize}

These can be put together using type constructors, including the function
constructor {\black \verb+->+} and the Cartesian product constructor {\black \verb+*+}.

We will see how to define other types and type constructors later.

\end{slide*}



\begin{slide*}

\heading{Infixes}

\vspace*{0.5cm}

Many built-in constants like {\black \tt +} have infix status. They also have a notion
of precedence, so expressions associate more or less as expected.

For example, {\black \tt x < 2 * y + z} is parsed as {\black \tt < x (+ (* 2 y)
z)}.

You can define your own infixes using the {\black \verb+#infix+} directive:

\begin{black}\begin{verbatim}
  #let o f g = fun x -> f(g x);;
  o : ('a -> 'b) -> ('c -> 'a) ->
      'c -> 'b = <fun>
  ##infix "o";;
  #let add2 = successor o successor;;
  add2 : int -> int = <fun>
  #add2 0;;
  - : int = 2
\end{verbatim}\end{black}

\end{slide*}


\begin{slide*}

\heading{Basic infix operators}

\begin{center}
\begin{tabular}{|l|l|}
\hline
Operator   & Meaning               \\
\hline
{\black \tt mod}  & Modulus (remainder)   \\
{\black \tt *}    & Multiplication        \\
{\black \tt /}    & Truncating division   \\
{\black \tt +}    & Addition              \\
{\black \tt -}    & Subtraction           \\
{\black \verb+^+} & String concatenation  \\
{\black \tt =}    & Equality              \\
{\black \tt <>}   & Inequality            \\
{\black \tt <}    & Less than             \\
{\black \tt <=}   & Less than or equal    \\
{\black \tt >}    & Greater than          \\
{\black \tt >=}   & Greater than or equal \\
{\black \tt \&}   & Boolean `and'         \\
{\black \tt or}   & Boolean `or'          \\
\hline
\end{tabular}
\end{center}

\end{slide*}



\begin{slide*}

\heading{Notes on operators}

\vspace*{0.5cm}

Note that the logical operators {\black \verb+&+} and {\black \verb+or+} also have a
non-eager evaluation strategy. You can regard them as synonyms:

\begin{black}
\begin{eqnarray*}
p \mbox{ \& } q & {\red \defeq} & \mbox{if } p \mbox{ then } q \mbox{ else false}  \\
p \mbox{ or } q & {\red \defeq} & \mbox{if } p \mbox{ then true else } q
\end{eqnarray*}
\end{black}

There are also two built-in symbolic operations on the basic types, {\black
\verb+-+}, which performs numerical negation, and {\black \tt not} which
performs logical negation.

The logical {\black \tt not} operator has special prefix status, so that {\black \tt not not
p} is parsed as {\black \tt not (not p)}. This reverses the usual left-associativity
convention for functions.

\end{slide*}


\begin{slide*}

\heading{Examples (1)}

\vspace*{0.5cm}

We define by recursion a function that takes a positive integer {\red $n$}
and a function {\red $f$} and returns {\red $f^n$}, i.e. {\red $f \circ \cdots
\circ f$} ({\red $n$} times):

\begin{black}\begin{verbatim}
  #let rec funpow n f x =
     if n = 0 then x
     else funpow (n - 1) f (f x);;
  funpow : int -> ('a -> 'a) ->
           'a -> 'a = <fun>
\end{verbatim}\end{black}

In fact, {\black \tt funpow} takes a machine integer {\black \tt n} to the
corresponding Church numeral. We can easily define an inverse function that
goes the other way:

\begin{black}\begin{verbatim}
  #let defrock n = n (fun x -> x + 1) 0;;
  defrock : ((int -> int) -> int -> 'a) ->
            'a = <fun>
  #defrock(funpow 32);;
  - : int = 32
\end{verbatim}\end{black}

\end{slide*}



\begin{slide*}

\heading{Examples (2)}

\vspace*{0.5cm}

Recall the arithmetic operators on Church numerals. We can test them:

\begin{black}\begin{verbatim}
  #let add m n f x = m f (n f x)
   and mul m n f x = m (n f) x
   and exp m n f x = n m f x;;
   and test bop x y =
     defrock (bop (funpow x) (funpow y));;
...
  #test add 2 10;;
  - : int = 12
  #test mul 2 10;;
  - : int = 20
  #test exp 2 10;;
  - : int = 1024
\end{verbatim}\end{black}

They seem to work. Of course they're not very efficient!

\end{slide*}



\begin{slide*}

\heading{Defining new types}

\vspace*{0.5cm}

ML has facilities for defining new types and type constructors.

In fact, the constructors can be recursive, i.e. not only take existing types
as arguments but the new type itself.

We will look at a simple example first: the disjoint sum type.

\begin{black}\begin{verbatim}
  #type ('a,'b)sum = inl of 'a
                   | inr of 'b;;
  Type sum defined.
\end{verbatim}\end{black}

This creates a new type {\black \tt sum} and two new {\em constructors}:

\begin{black}\begin{verbatim}
  #inl;;
  - : 'a -> ('a, 'b) sum = <fun>
  #inr;;
  - : 'a -> ('b, 'a) sum = <fun>
\end{verbatim}\end{black}

\end{slide*}


\begin{slide*}

\heading{Properties of type constructors}

\vspace*{0.5cm}

All type constructors arising in this way have three key properties:

\begin{enumerate}

\item They are exhaustive, i.e. every element of the new type is obtainable
either by  {\black \tt inl x} for some {\black \tt x} or {\black \tt inr y} for some {\black \tt y}.

\item They are injective, i.e. an equality test {\black \tt inl x = inl y} is true if
and only if {\black \tt x = y}, and similarly for {\black \tt inr}.

\item They are distinct, i.e. their ranges are disjoint. More concretely this
means in the above example that {\black \tt inl x = inr y} is false whatever {\black \tt x}
and {\black \tt y} might be.

\end{enumerate}

Because of these properties, we can define functions by {\em pattern matching}.

\end{slide*}




\begin{slide*}

\heading{Pattern matching}

\vspace*{0.5cm}

We perform pattern matching by using more general expressions called {\em
varstructs} as the arguments to lambdas. We can also consider several different
cases. For example:

\begin{black}\begin{verbatim}
  #fun (inl n) -> n > 6
     | (inr b) -> b;;
  - : (int, bool) sum -> bool = <fun>
\end{verbatim}\end{black}

This function has the property, naturally enough, that when applied to {\black
\tt inl n} it returns {\black \verb+n > 6+} and when applied to {\black \tt inr
b} it returns {\black \tt b}. Why is this valid?

It is permissible to recover {\black \tt n} from {\black \tt inl n} because the
constructors are injective. The cases cannot clash because the constructors are
distinct. Finally, the function is defined everywhere because the constructors
are exhaustive.

\end{slide*}




\begin{slide*}

\heading{Non-exhaustive matching}

\vspace*{0.5cm}

In fact, we can define partial functions that don't cover every case:

\begin{black}\begin{verbatim}
  #fun (inr b) -> b;;
  Toplevel input:
  >fun (inr b) -> b;;
  >^^^^^^^^^^^^^^^^
  Warning: this matching is not exhaustive.
  - : ('a, 'b) sum -> 'b = <fun>
\end{verbatim}\end{black}

The compiler warns us of this fact. If we try to use the function on an
argument not of the form {\black \tt inl x}, then it will not work:

\begin{black}\begin{verbatim}
  #(...) (inl 3);;
  Uncaught exception: Match_failure
\end{verbatim}\end{black}

\end{slide*}




\begin{slide*}

\heading{General matching}

\vspace*{0.5cm}

We can perform matching even in other situations, when the matches might not be
mutually exclusive. In this case, the first possible match is taken.

\begin{black}\begin{verbatim}
  #(fun 0 -> true | n -> false) 0;;
  - : bool = true
  #(fun 0 -> true | n -> false) 1;;
  - : bool = false
\end{verbatim}\end{black}

However, in general, constants need special constructor status, or they will be
treated just as variables for binding:

\begin{black}\begin{verbatim}
  #(fun true -> 1 | false -> 0) (4 < 3);;
  - : int = 0
  #let true_1 = true and false_1 = false in
  (fun true_1 -> 1 | false_1 -> 0) (4 < 3);;
  - : int = 1
\end{verbatim}\end{black}

\end{slide*}


\begin{slide*}

\heading{Other matching constructs}

\vspace*{0.5cm}

Instead of using {\black \tt fun} with various patterns, and applying the
function to an expression, there is an alternative syntax that uses the
expression directly:
{\black $$ \mbox{match}\; E\; \mbox{with}\;
   pattern_1 \mbox{\verb+->+} E_1 \mid \cdots \mid
   pattern_n \mbox{\verb+->+} E_n $$}
The simplest alternative of all is to use
{\black $$ \mbox{let}\; pattern \mbox{ = } expression $$}
\noindent but in this case only a single pattern is allowed. For example:

\begin{black}\begin{verbatim}
  #let (inl x) = inl 3;;
  Toplevel input:
  >let (inl x) = inl 3;;
  >^^^^^^^^^^^^^^^^^^^^^
  Warning: this matching is not exhaustive.
  x : int = 3
\end{verbatim}\end{black}

\end{slide*}



\begin{slide*}

\heading{Recursive types}

\vspace*{0.5cm}

As we have said, types can be defined recursively, i.e. in terms of themselves.

\begin{black}\begin{verbatim}
  #type ('a)list = Nil
                 | Cons of 'a * ('a)list;;
  Type list defined.
  #Nil;;
  - : 'a list = Nil
  #Cons;;
  - : 'a * 'a list -> 'a list = <fun>
\end{verbatim}\end{black}

We imagine {\black \tt Nil} as the empty list and {\black \tt Cons} as a
function that adds a new element on the front of a list. The lists {\black \tt
$[]$}, {\black \tt $[1]$}, {\black \tt $[1;2]$} and {\black \tt $[1;2;3]$} are
written:

\begin{black}\begin{verbatim}
  Nil;;
  Cons(1,Nil);;
  Cons(1,Cons(2,Nil));;
  Cons(1,Cons(2,Cons(3,Nil)));;
\end{verbatim}\end{black}

\end{slide*}




\begin{slide*}

\heading{Lists}

\vspace*{0.5cm}

Actually, this type is already built in. The empty list is written {\black \verb+[]+}
and the recursive constructor {\black \verb+::+}, has infix status. Thus, the above
lists are actually written:

\begin{black}\begin{verbatim}
  #[];;
  - : 'a list = []
  #1::[];;
  - : int list = [1]
  #1::2::[];;
  - : int list = [1; 2]
  #1::2::3::[];;
  - : int list = [1; 2; 3]
\end{verbatim}\end{black}

The version that is printed can also be used for input:

\begin{black}\begin{verbatim}
  #[1;2;3;4;5] = 1::2::3::4::5::[];;
  - : bool = true
\end{verbatim}\end{black}


\end{slide*}





\begin{slide*}

\heading{Pattern matching over lists}

\vspace*{0.5cm}

We can now define functions by pattern matching in the usual way. For example,
we can define functions to take the head and tail of a list:

\begin{black}\begin{verbatim}
  #let hd (h::t) = h;;
  Toplevel input:
  >let hd (h::t) = h;;
  >    ^^^^^^^^^^^^^
  Warning: this matching is not exhaustive.
  hd : 'a list -> 'a = <fun>
  #let tl (h::t) = t;;
  Toplevel input:
  >let tl (h::t) = t;;
  >    ^^^^^^^^^^^^^
  Warning: this matching is not exhaustive.
  tl : 'a list -> 'a list = <fun>
\end{verbatim}\end{black}

ML warns us that they will fail when applied to an empty list.

\end{slide*}



\begin{slide*}

\heading{Recursive functions over lists}

\vspace*{0.5cm}

It is possible to mix pattern matching and recursion. This is natural since the
type itself is defined recursively. For example, here is a
function to return the length of a list:

\begin{black}\begin{verbatim}
  #let rec length =
     fun [] -> 0
       | (h::t) -> 1 + length t;;
  length : 'a list -> int = <fun>
  #length [];;
  - : int = 0
  #length [5;3;1];;
  - : int = 3
\end{verbatim}\end{black}

Alternatively, this can be written in terms of our earlier `destructor'
functions {\black \tt hd} and {\black \tt tl}. This style of function definition is more
usual in many languages, notably LISP, but the direct use of pattern matching
is often more elegant.

\end{slide*}




\begin{slide*}

\heading{The subtlety of recursive types}

\vspace*{0.5cm}

Consider the following:

\begin{black}\begin{verbatim}
  #type ('a)embedding =
     K of ('a)embedding->'a;;
\end{verbatim}\end{black}

This looks suspicious because it embeds the function space {\red $A \to B$}
inside {\red $A$}. In fact it only embeds the {\em computable} functions.
We must be careful with semantics, and also types:
\begin{black}\begin{verbatim}
  #let Y h =
    let g (K x) z = h (x (K x)) z in
    g (K g);;
  Y : (('a -> 'b) -> 'a -> 'b) ->
      'a -> 'b = <fun>
  #let fact = Y (fun f n ->
     if n = 0 then 1 else n * f(n - 1));;
  fact : int -> int = <fun>
  #fact 6;;
  - : int = 720
\end{verbatim}\end{black}

\end{slide*}




\end{document}
